\begin{tabbing}
$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$), $n$:$\mathbb{N}$.
\\[0ex]False
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$(ecl{-}trans{-}h($A$)($n$,ecl{-}trans{-}init($A$)))))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]($\neg$(ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,$L$)))
\\[0ex]$\Rightarrow$ \=($\forall$$L_{1}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]$L_{1}$ $\leq$ $L$ $\Rightarrow$ ($\uparrow$(ecl{-}trans{-}h($A$)($n$,ecl{-}trans{-}state($A$;$L_{1}$)))) $\Rightarrow$ False))
\-\-
\end{tabbing}